Inference at * 2 2 1 1 
Iof proof for Lemma p-fun-exp-add-sq:

.....equality..... NILNIL

1. A : Type
2. f : A(A + Top)
3. x : A
4. m : 
5. 0 < m
6. n:. (can-apply(f^m - 1;x))  ((f^n+(m - 1)(x)) ~ (f^n(do-apply(f^m - 1;x))))
7. n : 
8. can-apply(f^m;x)
9. (n = 0)
10. (n+m = 0)
11. (n = 0)
12. (m = 0)
  (f o f^(n+m) - 1  (x)) ~ (f o f^n  (do-apply(f^m - 1;x))) 

latex

 by ((Unfold `p-compose` ( 0)) 
CollapseTHEN (RepUR ``can-apply do-apply`` ( 0))) 

CoCollapseTHEN ((Subst' ((n+m) - 1) ~ (n+(m - 1)) ( 0)) 
CollapseTHEN (((Try ((Complete (Auto))
C))) 
CollapseTHEN ((Subst' (f^n+(m - 1)(x)) ~ (f^n(do-apply(f^m - 1;x))) ( 0)) 
CollapseTHEN (
C((Try ((Fold `do-apply` 0) 
CollapseTHEN (Trivial)))) 
CollapseTHEN ((if ((0
C) = 0) then BackThruSomeHyp else BHyp (0) )))))) 

latex

C1: 

C1:   can-apply(f^m - 1;x)
C.

Definitions

s ~ t, n+m, f(a), do-apply(f;x), f^n, n - m, #$n, f o g  , can-apply(f;x), if b then t else f fi , t  T, SQType(T), s = t, left + right, Top, , {x:A| B(x)} , , A  B, A, False, {T}, x:A. B(x), P  Q